Left Termination of the query pattern
subset(g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 83 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 75 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 PiDPToQDPProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QDPSizeChangeProof (⇔, 0 ms)
        ↳18 YES

(0) Obligation:

Clauses:

member(X, .(Y, Xs)) :- member(X, Xs).
member(X, .(X, Xs)).
subset(.(X, Xs), Ys) :- ','(member(X, Ys), subset(Xs, Ys)).
subset([], Ys).

Query: subset(g,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

memberB(X1, .(X2, X3)) :- memberB(X1, X3).
subsetA(.(X1, X2), .(X3, X4)) :- memberB(X1, X4).
subsetA(.(X1, X2), .(X3, X4)) :- ','(membercB(X1, X4), subsetA(X2, .(X3, X4))).
subsetA(.(X1, X2), .(X1, X3)) :- subsetA(X2, .(X1, X3)).

Clauses:

subsetcA(.(X1, X2), .(X3, X4)) :- ','(membercB(X1, X4), subsetcA(X2, .(X3, X4))).
subsetcA(.(X1, X2), .(X1, X3)) :- subsetcA(X2, .(X1, X3)).
subsetcA([], X1).
membercB(X1, .(X2, X3)) :- membercB(X1, X3).
membercB(X1, .(X1, X2)).

Afs:

subsetA(x1, x2)  =  subsetA(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
subsetA_in: (b,b)
memberB_in: (b,b)
membercB_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U2_GG(X1, X2, X3, X4, memberB_in_gg(X1, X4))
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → MEMBERB_IN_GG(X1, X4)
MEMBERB_IN_GG(X1, .(X2, X3)) → U1_GG(X1, X2, X3, memberB_in_gg(X1, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → U4_GG(X1, X2, X3, X4, subsetA_in_gg(X2, .(X3, X4)))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → U5_GG(X1, X2, X3, subsetA_in_gg(X2, .(X1, X3)))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))

The TRS R consists of the following rules:

membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))

Pi is empty.
We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U2_GG(X1, X2, X3, X4, memberB_in_gg(X1, X4))
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → MEMBERB_IN_GG(X1, X4)
MEMBERB_IN_GG(X1, .(X2, X3)) → U1_GG(X1, X2, X3, memberB_in_gg(X1, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → U4_GG(X1, X2, X3, X4, subsetA_in_gg(X2, .(X3, X4)))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → U5_GG(X1, X2, X3, subsetA_in_gg(X2, .(X1, X3)))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))

The TRS R consists of the following rules:

membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 5 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)

The TRS R consists of the following rules:

membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))

The TRS R consists of the following rules:

membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(15) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))

The TRS R consists of the following rules:

membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))

The set Q consists of the following terms:

membercB_in_gg(x0, x1)
U10_gg(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(17) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
    The graph contains the following edges 2 >= 1

  • SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))
    The graph contains the following edges 1 > 1, 2 >= 2

  • SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
    The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 2 > 4

(18) YES